Integrated circuits (ICs) have become the backbone of modern consumer electronics. The increased demand for functionality of consumer electronics has forced the complexity of IC's to skyrocket. In a number of applications, ICs must be highly functional, low cost and have low power consumption. These demands create increased complexity on the design, verification, and manufacture of ICs. These increases in complexity have significantly exacerbated the difficulties associated with verification of the designs.
There are a number of computer aided techniques that are typically used to verify the functionality of digital designs. For example, model checking is a widely used formal verification technique that may be implemented with Binary Decision Diagrams (BDD). As is known in the art, BDDs are data structures used to represent Boolean functions. With recent advances in tools to solve the Boolean satisfiability problem (SAT), SAT solvers are proving to be an effective alternative to BDD's. A given Boolean formula is considered satisfiable if all the variables in the formula can take on such values to make the formula evaluate to true. Alternatively, and potentially more important, if no combination of values can be found that forces the function to evaluate to true, then the formula is unsatisfiable. With complex digital designs, verification approaches can be significantly complex and the memory limits of a computer can be quickly reached.
In Bounded Model Checking (BMC) a system is typically unfolded “k” times and encoded as a SAT problem to be solved by a SAT solver. SAT solvers typically require the function to be expressed in Conjunctive Normal Form (CNF) which is a conjunction of clauses, where a clause is a disjunction of literals. A literal is either a variable name or its negation. A satisfying assignment returned by the SAT solver corresponds to a counterexample of length k. If the problem is unsatisfiable at length k, the SAT returns a proof that there are no counterexamples of length k. BMC, while successful in finding errors is incomplete in the sense that there is no efficient way to decide that a property is true.
Additionally, there are a number of Unbounded Model Checking (UMC) techniques that make use of the SAT-based BMC in some way. Of particular interest are the “proof-based abstraction” and the “interpolation-based” techniques. The proof-based abstraction algorithm is an iterative abstraction refinement method that typically uses a traditional BDD-based model checker to prove properties of the abstract models. In this approach an initial BMC run is accomplished, if the problem proved unsatisfiable, the resulting proof is used to guide the formulation of a new abstraction. The refinement technique typically removes parts of the design under verification such that if the property is true in the abstraction that implies that it is true in the actual design. Abstraction refinement is an iterative method that tries to prove the property on an abstraction and if a property is found to be false, a concretization step is done to determine if the failure is real, otherwise the abstraction is refined and the procedure is continued. The concretization step involves reasoning about the actual design and is most often done by employing BMC at the depth of the counterexample. As designs get larger and the counterexample depths increases, this approach can lead to significant difficulties in terms of time required to verify a design and memory constraints of the computer running the verification.
The interpolation-based model checking algorithm is a purely Boolean satisfiability (SAT) based model checking method that does not rely on abstraction refinement, though like abstraction methods, it tends to work well on properties that are localizable, and is fairly insensitive to the addition of irrelevant logic. This method uses BMC to find failures and proves properties by doing a SAT-based approximate reachability analysis. While proof-based methods do better on problems where BDDs are particularly effective, interpolation methods have advantages with larger problems. Interpolation based algorithms are fairly insensitive to irrelevant logic but once again are time and resource intensive.
Further, hybrid verification techniques exist that attempt to combine various BDD and SAT-based techniques. In one such technique conflict clauses that were learned from BDDs are used to improve the performance of SAT BMC. Another method uses BDDs to compute an over-approximation of the reachable states and applies these constraints to the SAT BMC problem. A further technique uses BDD-based reachability analysis to compute lower bounds on reachable states to accelerate SAT-based induction. Proof-based and counterexample-based abstraction methods have been combined in different phases of an iterative abstraction refinement process. One hybrid method uses a single abstraction phase that is intermediate between the proof-based and counterexample-based abstraction refinement. Abstraction refinement has also been used with BMC to find failures more effectively. A recent technique combines abstraction refinement and interpolation in a manner which is similar to using interpolation as the UMC in a proof-based technique. Most of these hybrid methods also require a significant amount of time and memory for verification. These issues pose significant limitations on the size of designs that can be verified.
Therefore there exists a need for more robust verification algorithms that can take advantage of these and other techniques to improve analysis time and fit within memory constraints.